i:Id, A:MsgA, M:System. (M(i) ||+ A)  M || @i: A 

latex

Definitions	MsgA, System, A || B, A ||+ B, @i: A, left+right, Unit, P  Q, a = b, , b, A, Type, b, x:AB(x), s ~ t, Prop, s = t, Id, SQType(T), P  Q, {T}, P & Q, M1 || M2, ma-frame-compatible(A;B), , f(a), x:A. B(x), x:AB(x), t  T
Lemmas	ma-empty-compatible-right, ma-empty-frame-compatible-right, Id sq, Id wf, assert wf, not wf, bnot wf, bool wf, eq id wf, assert-eq-id, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, ma-compat wf, msystem wf, msga wf